![[TLA+] ダイ・ハードジャグ問題から仕様を考える](https://devio2023-media.developers.io/wp-content/uploads/2019/01/TLA_logo_splash_image_3.png){kind=logo}
[TLA+] ダイ・ハードジャグ問題から仕様を考える
こむろ＠事業開発部です。今の時期、札幌にはスギ花粉がほとんどありません。花粉症に悩まされることがないのはとても嬉しい。
基本的にLamport先生が公開しているVideoレクチャーを自分なりに解釈して、再度解説することで記事を書いています。Leslie Lamport先生はなかなかユニークな授業を展開しています。 *1
今回はなんと映画ダイ・ハード3の「ジャグ問題」を題材に仕様をTLA+で表現します。
Die hard 3 Jugs Problems
ダイ・ハード3のジャグ問題については、こちらのリンクを参照します。自分はあまり知らなかったのですが結構有名なんでしょうか。ダイ・ハード3の1シーンから。ざっと概要を説明すると
- ちょうど4ガロンの水を入れないと爆弾が爆発する
- ただし今手元にあるのは3ガロンと5ガロンのジャグしかない
- どういう手順を踏めばちょうど4ガロンを測れるか
わかり易い問題です。皆さんが普段得意としているプログラミング言語ならば、ものの数分程度で解けるのではないでしょうか。
TLA+で状態を考える
TLA+ではすべての状態を定義し、その定義から外れる状態がないか、条件に違反する状態がないかを総チェックできることを確認しました。5ガロンと3ガロンのジャグを使ったすべての状態を記載してみましょう。
以下のような状態遷移が考えられます。
これらの状態をTLA+で記述します。
DieHard Specを作成する
TLA+を起動し、新しいSpecを作成します。今回は DieHard というモジュール名にします。
------------------------------ MODULE DieHard ------------------------------ EXTENDS Integers VARIABLES small, big =============================================================================
利用する変数は5ガロンのジャグを示す big, 3ガロンのジャグを示す small を定義します。今回は以上です。前回と同じく数値の算術を行うため Integers モジュールをインポートします。
各ステップで変数が違反していないかをチェックする
TLA+には型チェックがありません。そのためその値が正しいかどうかを言語的にチェックすることができません。そのため、TLA+ではすべての状態において必ず条件が満たされる式を定義することでAssertionすることができます。今回は TypeOK という式で定義します。この式は常にすべてのステップにおいて真になることが求められます。
使用するジャグは5ガロンと3ガロンです。当然ながら限界の水を超えてジャグに入れることはできません。この上限値の制限を定義します。では TypeOK を定義しましょう。
------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small, big
TypeOK == /\ small \in 0..3
/\ big \in 0..5
=============================================================================
この式を満たす条件は small は {0, 1, 2, 3} のいずれかである必要があります。同じく big は {0, 1, 2, 3, 4, 5} を常に満たす必要があります。つまりこの変数は数字でかつ決められた値の範囲以外を取ることは許されません。
初期状態を定義
初期状態を定義します。はじめはそれぞれのジャグには水が入っていないため以下のようになります。
------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small, big
TypeOK == /\ small \in 0..3
/\ big \in 0..5
Init == /\ small = 0
/\ big = 0
=============================================================================
いずれも特に疑問はなさそう。
次状態を定義
初期状態がわかったので状態の総数をすべて考えてみましょう。考えうる状態は3状態です。
- ジャグが空 (Small / Big)
- ジャグが満杯 (Small / Big)
- 片方のジャグから片方のジャグへ移す (Small / Big)
上記 3状態 はそれぞれ2つの変数が関わります。ひとまず未定義の式を状態ごとに羅列します。
------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small, big
TypeOK == /\ small \in 0..3
/\ big \in 0..5
Init == /\ small = 0
/\ big = 0
Next == \/ FillSmall \* Smallジャグが満杯（Bigの状態は知らん）
\/ FillBig \* Bigジャグが満杯（Smallの状態は知らん）
\/ EmptySmall \* Smallジャグが空（同上）
\/ EmptyBig \* Bigジャグが空（同上）
\/ SmallToBig \* SmallからBigへ水を移動する
\/ BigToSmall \* BigからSmallへ水を移動する
=============================================================================
それぞれの状態の和集合を取ります。（ \/ つまり OR）
Fill{Small, Big}, Empty{Small, Big}
Small, Big それぞれのジャグが満杯になる状況を記述します。
FillSmall == small' = 3 FillBig == big' = 5
プログラマーな思考で書くとこれで問題ありません。しかし、これは正しく動作しません。なぜならば big の状態が定義されていません。TLA+では以下のように記述します。
FillSmall == /\ small' = 3
/\ big' = big \* bigジャグは変化しない
big の次状態は現状態の big の値をそのまま入力する式を記載します。VideoでもLamport先生が話していますが、これは厳密に数学ではなく 「That's a bad idea」 であるとのこと。
FillBig も同じように式を定義します。
FillBig == /\ big' = 5
/\ small' = small
同じ要領で Empty シリーズの式も定義します。
EmptySmall == /\ small' = 0
/\ big' = big
EmptyBig == /\ big' = 0
/\ small' = small
変数の並びが big, small がそれぞれの式でひっくり返っていますが、それぞれ交換則が成り立つので式を入れ替えも可能です。いずれも結果は変わりません。これでそれぞれ満杯、および空の状況をすべて記述できました。次は中途半端な状態を記述します。
SmallToBig, BigToSmall
片方のジャグから片方のジャグへ水を移動させる場合を考えていきます。まずは Small から Big へ水を移動させる状況を考えてみます。以下の2パターンが考えられます。
水を移した結果、Big ジャグから漏れるか、漏れないかで場合分けができそうです。TLA+で記述していきましょう。
SmallToBig == IF big + small =< 5
THEN /\ big' = big + small \* ここが実際に評価される式
/\ small' = 0
ELSE /\ big' = 5 \* ここが実際に評価される式
/\ small' = big + small - 5
TLA+では IF THEN ELSE で分岐を表現できます。今回は5ガロンを超えるかどうかで分岐を記載します。 条件によって評価される式のセットが切り替わります。SmallToBig では現状態の値によって式が切り替わります。
/\ big' = big + small /\ small' = 0
か
/\ big' = 5 /\ small' = big + small - 5
が選択されて評価されます。
続いて同じように BigToSmall を記述します。まずはイメージ
ここでは3ガロンが分岐条件となります。TLA+で記述します。
BigToSmall == IF big + small <= 3
THEN /\ small' = big + small
/\ big' = 0
ELSE /\ small' = 3
/\ big' = big + small - 3
big から small への移動なので原則的に small がどうなるかを中心に式を組みました。
さてこれで未定義の式はありません。すべての状態を記述できました。
全ての式を定義したコードは以下のようになります。
------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small, big
TypeOK == /\ small \in 0..3
/\ big \in 0..5
Init == /\ big = 0
/\ small = 0
FillSmall == /\ small' = 3
/\ big' = big \* thats a bad idea. It's not math
FillBig == /\ big' = 5
/\ small' = small \* thats a bad idea. It's not math
EmptySmall == /\ small' = 0
/\ big' = big
EmptyBig == /\ big' = 0
/\ small' = small
SmallToBig == IF big + small =< 5
THEN /\ big' = big + small
/\ small' = 0
ELSE /\ big' = 5
/\ small' = big + small - 5
BigToSmall == IF big + small <= 3
THEN /\ small' = big + small
/\ big' = 0
ELSE /\ small' = 3
/\ big' = big + small - 3
Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
NotSolved == big /= 4
=============================================================================
\* Modification History
\* Last modified Fri Feb 22 22:10:06 JST 2019 by komurohiraku
\* Created Sat Jan 05 23:43:04 JST 2019 by komurohiraku
LaTeXでの表記も載せておきます。
評価する
ではモデルを作成して評価しましょう。Model_1 を追加します。
今回は特に変更をせずにモデル検査を実行します。実行ボタン をクリックします。
結果は以下の通り。
モデル検査が完了しました。No Errors なので問題なく終了しました。が、はてさてこれで何がわかったのでしょうか。
この検査結果を通してわかったこと
この検査を行うことで、5ガロンのBigジャグ、3ガロンのSmallジャグの起こりうる全ての状態を検査します。
つまりここで確認しているのは 4ガロンになる組み合わせを探すことを目的としてるわけではありません。 つまり、パラメータの範囲内で考えうる全ての状態が、式で表記した 状態 からいずれも外れないことが確認できました。
記述した式で全ての状態を表現できることが証明できたことになります。
4ガロンになる最短の組み合わせを検査する
全ての状態が列挙できて表現できたのは良いとして、爆弾を正常に処理するためには4ガロンの水を正確に測るための最短手順が気になるところです。
TLA+は論理演算です。そのため、全ての式は真偽で表現されます。そのため、4ガロンになった瞬間に探索を停止させましょう。以下の式を追加します。
NotSolved == big # 4
# は ≠ です。別の書き方として /= でも同意です。いずれも Not Equal となります。すなわちこの式は big が 4 になった状態で False となります。
この式を Model_1 のOverviewにある Invariants に設定します。
Add をクリックして式の名前を追加。
このようにInvariantsに NotSolved が入力され、チェックされている状態を作ります。
Invariantsについて
ところでInvariantsはどんな式がどのように評価されるのでしょうか。
Invariantsは全てのステップで常に真でないといけない式を定義する箇所になります。
決して破ってはいけない原則、例えば「全てのステップにおいて Small + Big <= 8 という式。つまり、 小さいジャグと大きいジャグを合わせて8ガロンを上回ってはいけない」という条件式を入力することができます。
再度モデル検査を実施する
さて、Invariantsに満たすべき式を追加しました。再度モデル検査を実行してみましょう。
ちょっと見づらいので右ペインを抜粋。
NotSolved の式が False になったため条件違反として検出されました。これが最短手順のようです。
ちなみに現在の TLC実行モード は幅優先探索(Breadth-first search)で全ての状態を探索しています。
まとめ
実際にある問題の仕様を記述し、すべての組み合わせが式で表現できることを確認しました。問題の解法を導き出すのではなく、どんなパラメータの組み合わせでも仕様から外れないことを確認するという、何を検証しているのかを理解するのがなかなか難しいところです。今回は非常に単純な問題でしたが、これらを徐々に実際の業務等に使えるような領域に適用する演習を詰んでいきたいところです。
結構楽しくなってきました。
次回はTransaction Commit。いよいよ情報処理の世界で適用できる演習が始まります。
参照
脚注
- 大学でこういう授業はとても楽しそう。 ↩
